A:Type, eq:EqDecider(A), B, C, D, E, F, G:(AType), f:a:A fp B(a), g:a:A fp C(a),
h:a:A fp D(a).
(a:A. B(a) r E(a))
 (a:A. C(a) r F(a))
 (a:A. D(a) r E(a))
 (a:A. D(a) r F(a))
 (a:A. F(a) r G(a))
 (a:A. E(a) r G(a))
 {h || f  h || g  h || f  g} 

latex

Definitions	x:A. B(x), x(s), {T}, EqDecider(T), strong-subtype(A;B), f || g, a:A fp B(a), Top, x. t(x), P  Q, f  g, f(x)?z, f(x), Unit, P  Q, x  dom(f), , , b, t  T, A, False, P  Q, P & Q, b
Lemmas	assert wf, not wf, bnot wf, bool wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-join-dom2, fpf-trivial-subtype-top, top wf, fpf-join wf, subtype rel transitivity, strong-subtype-self, subtype-fpf3, deq wf, fpf wf, fpf-compatible wf, fpf-ap wf